COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE INDVAR Q3 Q4 εLEGALPOSTION
C00020 ENDMK
C⊗;
DECLARE INDVAR Q3 Q4 εLEGALPOSTION;
DEFINE QBUDTAKES:
∀P Z YYW.((BOARD(P,QBUD)∧POS(P,'(2 . 4))=Z∧POS(P,'(5 . 8))=YYW)⊃∃Q1 Q2
Q3 Q4 X1 X2 X3 X4.(((PREDEGAME(Q1,P)∨Q1=P)∧TAKINGS MOVE Q1∧MOVER MOVE Q1
=BQNP∧TO MOVE Q1='(3 . 1)∧TAKEN MOVE Q1=X1)∧(((PREDEGAME(Q2,P)∨Q2=P)∧
TAKINGS MOVE Q2∧MOVER MOVE Q2=BKBP∧TO MOVE Q2='(3 . 5)∧TAKEN MOVE Q2=X2)
∧(((PREDEGAME(Q3,P)∨Q3=P)∧TAKINGS MOVE Q3∧MOVER MOVE Q3=BKBP∧TO MOVE Q3
='(4 . 4)∧TAKEN MOVE Q3=X3)∧(((PREDEGAME(Q4,P)∨Q4=P)∧TAKINGS MOVE Q4∧
MOVER MOVE Q4=BKBP∧TO MOVE Q4='(5 . 3)∧TAKEN MOVE Q4=X4)∧(((X1=WKB∨X1=
WQ∨X1=WKR∨X1=WQR∨X1=WKN∨X1=WQN)∧(¬X1=YYW∧¬X1=Z))∧(((X2=WKB∨X2=WQ
∨X2=WKR∨X2=WQR∨X2=WKN∨X2=WQN)∧(¬X2=YYW∧¬X2=Z))∧(((X3=WKB∨X3=WQ
∨X3=WKR∨X3=WQR∨X3=WKN∨X3=WQN)∧(¬X3=YYW∧¬X3=Z))∧(((X4=WKB∨X4=WQ∨
X4=WKR∨X4=WQR∨X4=WKN∨X4=WQN)∧(¬X4=YYW∧¬X4=Z))∧¬X1=X2∧¬X1=X3
∧¬X1=X4∧¬X2=X3∧¬X2=X4∧¬X3=X4))))))));;
MARK M2;
DEFINE WCAPTURETHM:
∀P SQ.(TO MOVE P=SQ⊃((ORDINARY MOVE P∧WVALUES PIECEON(TBOARD PREVPOS P,SQ))⊃
		CAPTURE MOVE P));;
DEFINE WKNPPATH:∀P Q SQ.((POS(Q,'(6 . 7))=WKNP∧POS(P,SQ)=WKNP∧
     PREDEGAME(P,Q)∧VALUEP VAL(Q,WKNP))⊃(SQ='(7 . 7)∨SQ='(6 . 7)));;
DEFINE WKRPPATH:∀P Q SQ.((POS(Q,'(7 . 8))=WKRP∧POS(P,SQ)=WKRP∧
     PREDEGAME(P,Q)∧VALUEP VAL(Q,WKRP))⊃(SQ='(7 . 8)∨SQ='(7 . 8)));;
DEFINE WKBPPATH:∀P Q SQ.((POS(Q,'(7 . 6))=WKBP∧POS(P,SQ)=WKBP∧
     PREDEGAME(P,Q)∧VALUEP VAL(Q,WKBP))⊃(SQ='(7 . 6)∨SQ='(7 . 6)));;
DEFINE BPAWNPATHTHM:
∀P X SQ1 SQ2.(MOVER MOVE P=X⊃(TO MOVE P=SQ2⊃(FROM MOVE P=SQ1⊃(VAL(PREVPOS
P,X)=PB⊃(¬(ROW(SQ2)=6)⊃(ORDINARY MOVE P∧((COLUMN(SQ1)=COLUMN(SQ2)∧(BSUC(
ROW(SQ1),ROW(SQ2))∧PIECEON(TBOARD PREVPOS P,SQ2)=MT))∨((COLUMN(SQ1)=COLUMN(
SQ2)∧(ROW(SQ1)=2∧(PIECEON(TBOARD PREVPOS P,SQ2)=MT∧(PIECEON(TBOARD PREVPOS 
P,MAKESQUARE(3,COLUMN(SQ1)))=MT∧ROW(SQ2)=4))))∨(TWOTOUCHING(COLUMN(SQ1),COLUMN
(SQ2))∧(BSUC(ROW(SQ1),ROW(SQ2))∧WVALUES PIECEON(TBOARD PREVPOS P,SQ2)))))))))));;
DEFINE XPATH:
∀Q P SQ SQ1 SQ2 X.(∀SQ.((MAY_PAWN_CAPTURES(SQ2,SQ,PIECECOLOR X)∧
    MAY_PAWN_CAPTURES(SQ,SQ1,PIECECOLOR X))⊃(SQ=SQ2∨SQ=SQ1))⊃
  ((POS(P0,SQ2)=X∧(POS(P,SQ1)=X∧(POS(Q,SQ)=X∧(PREDEGAME(Q,P)∧VALUEP VAL(P,X)))))⊃
(SQ=SQ2∨SQ=SQ1)));;
AXIOM PMOVING2:
	∀ B SQ1 SQ2.(WPAWNMOVE(B SQ1 SQ2)≡
	    (
		 ((COLUMN(SQ1)=COLUMN(SQ2)∧
		   WSUC(ROW(SQ1),ROW(SQ2))∧
		   PIECEON(B SQ2)=MT)  ∨
		  (COLUMN(SQ1)=COLUMN(SQ2)∧
		   ROW(SQ1)=7∧
		   PIECEON(B MAKESQUARE(6 COLUMN(SQ1)))=MT∧
		   ROW(SQ2)=5)∨
		   PIECEON(B SQ2)=MT∧
		  (TWOTOUCHING(COLUMN(SQ1),COLUMN(SQ2))∧
		   WSUC(ROW(SQ1),ROW(SQ2))∧
		   BVALUES(PIECEON(B SQ2))))));;

AXIOM PMOVING3:
	∀ B SQ1 SQ2.(BPAWNMOVE(B SQ1 SQ2)≡
	    (
		 ((COLUMN(SQ1)=COLUMN(SQ2)∧
		   BSUC(ROW(SQ1),ROW(SQ2))∧
		   PIECEON(B SQ2)=MT)  ∨
		  (COLUMN(SQ1)=COLUMN(SQ2)∧
		   ROW(SQ1)=2∧
		   PIECEON(B SQ2)=MT∧
		   PIECEON(B MAKESQUARE(3 COLUMN(SQ1)))=MT∧
		   ROW(SQ2)=4)∨
		  (TWOTOUCHING(COLUMN(SQ1),COLUMN(SQ2))∧
		   BSUC(ROW(SQ1),ROW(SQ2))∧
		   WVALUES(PIECEON(B SQ2))))));;
DEFINE DIFFTAKE:
∀P1 P2 Q X Y.((((P2=Q∨PREDEGAME(P2,Q))∧(P1=Q∨PREDEGAME(P1,Q)))∧((¬(TO MOVE
P1=TO MOVE P2)∨(¬(MOVER MOVE P1=MOVER MOVE P2)∨(PREDEGAME(P1,P2)∨¬(P1=P2
))))∧(TAKEN MOVE P1=X∧TAKEN MOVE P2=Y)))⊃¬(X=Y));;
DECLARE INDVAR Q4 ε LEGALPOSITION;
DEFINE TRANSPOS9:∀R B SQ.((BOARD(R,B)∧PIECEVALUES PIECEON(B,SQ))⊃CHESSPIECES POS(R,SQ));;
DEFINE MAYRW:∀R T.(VAL(R,T)=RW⊃((T=WKR∨T=WQR)∨(WPAWNS T∧PROMOTEDPAWN(R,T))));;
DEFINE BKRP8THM:∀Q P.((PAWNPROM MOVE Q∧(PREDEGAME(Q,P)∨Q=P)∧
	MOVER MOVE Q=BKRP∧¬TO MOVE Q='(8 . 7)∧¬TO MOVE Q='(8 . 8))⊃
    ∃Q1 Q2 X1 X2.((PREDEGAME(Q1,P)∨Q1=P)∧PREDEGAME(Q2,P)∧TAKINGS MOVE Q1∧
	TAKINGS MOVE Q2∧MOVER MOVE Q1=BKRP∧MOVER MOVE Q2=BKRP∧PREDEGAME(Q2,Q1)∧
	TAKEN MOVE Q1=X1∧TAKEN MOVE Q2=X2∧WHITEPIECE X1∧WHITEPIECE X2));;
DEFINE NEED2:∀SQ.((LASTRANKER(SQ,BLACK)∧(¬(SQ='(8 . 7))∧¬(SQ='(8 . 8))))⊃
	PAWNCAPTURES(SQ,'(2 . 8))≥2);;
DEFINE AINTMEBABE:∀Q P YYW Z X.(((Q=P∨PREDEGAME(Q P))∧TAKEN MOVE Q=X∧
    WHITEPIECE X∧BOARD(P QBUD)∧POS(P '(5.8))=YYW∧POS(P '(2.4))=Z)⊃
	((X=WQB∨X=WKB∨X=WQ∨X=WKR∨X=WQR∨X=WKN∨X=WQN)∧¬X=YYW∧¬X=Z));;
DEFINE DIFFTAKE:∀P1 P2 Q X Y.(((PREDEGAME(P2,Q)∧PREDEGAME(P1,Q))∧
	(¬TO MOVE P1=TO MOVE P2∨¬MOVER MOVE P1=MOVER MOVE P2∨
	 PREDEGAME(P1 P2)∨¬P1=P2)∧
	(TAKEN MOVE P1=X∧TAKEN MOVE P2=Y))⊃¬(X=Y));;
DEFINE SIMPTW:∀T.(WHITEPIECE T≡(
     T=WKP∨T=WQP∨T=WKNP∨T=WKBP∨T=WKRP∨T=WQBP∨T=WQNP∨T=WQRP∨
     T=WK ∨T=WQ ∨T=WKN ∨T=WKB ∨T=WKR ∨T=WQB ∨T=WQN ∨T=WQR));;
DEFINE DIE_ONCE:∀Q P X.(TAKEN MOVE P=X⊃(PREDEGAME(Q,P)⊃¬(TAKEN MOVE Q=X)));;
DEFINE WASON:∀P X.(TAKEN MOVE P=X⊃∃SQ.POS(PREVPOS P SQ)=X);;
AXIOM MCONSEQG:∀R T SQ.((¬TAKINGS MOVE R⊃¬T=TAKEN MOVE R)∧
			(¬ENPASSANT MOVE R⊃¬SQ=TAKENON MOVE R)∧
			(¬LEGALPOSITION R⊃¬MOVES MOVE R)∧
			(¬LEGALPOSITION R⊃¬SQ=TO MOVE R)∧
			(¬LEGALPOSITION R⊃¬SQ=FROM MOVE R)∧
			(¬LEGALPOSITION R⊃¬T=MOVER MOVE R)∧
			(¬CASTLE MOVE R⊃(¬SQ=ALSOTO MOVE R∧¬T=ALSOMOVER MOVE R)));;
AXIOM MCONSEQFA:
	∀R R1 SQ X.(((R1=R∨PREDEGAME(R1 R))∧TAKEN(MOVE(R1))=X)⊃
			¬POS(R SQ)=X);;
DEFINE CI:(α P0∧∀R P.((α R∧SUCCESSOR(R P))⊃α P))⊃∀R.α R;;
AXIOM CHESS_INDUCTION:
∀R.((α R∧∀R1 P2.((α R1∧(PREDEGAME(R R1)∨R=R1)∧SUCCESSOR(R1 P2))⊃α P2))⊃
	∀R2.((PREDEGAME(R R2)∨R=R2)⊃α R2));;
DEFINE PREPRED:
	∀R Q P.((SUCCESSOR(R Q)∧PREDEGAME(Q P))⊃PREDEGAME(R P)),
	∀Q P.(PREDEGAME(Q P)⊃PREDEGAME(PREVPOS Q P));;
DEFINE TAKEN_ON:
∀R Q Y X SQ.(PREVPOS Q=R⊃(TO MOVE Q=SQ⊃(MOVER MOVE Q=Y⊃
  ((TAKEN MOVE Q=X∧¬WHITEPIECE Y)⊃(WHITEPIECE X∧(¬ROW(SQ)=6⊃POS(R SQ)=X)))))),
∀R Q Y X SQ.(PREVPOS Q=R⊃(TO MOVE Q=SQ⊃(MOVER MOVE Q=Y⊃
  ((TAKEN MOVE Q=X∧WHITEPIECE Y)⊃(¬WHITEPIECE X∧(¬ROW(SQ)=3⊃POS(R SQ)=X))))));;
DEFINE WHICHWP:∀P SQ.(BOARD(P QBUD)⊃(WPAWNS POS(P SQ)≡
(SQ='(7.1)∨SQ='(7.8)∨SQ='(6.7)∨SQ='(6.2)∨SQ='(6.4)∨SQ='(7.3)∨SQ='(7.6)∨SQ='(2.3))));;
DEFINE MCONSEQKX:∀R P.((SUCCESSOR(R,P)∧ORDINARY MOVE P)⊃
     (¬(FROM MOVE P=TO MOVE P)∧
     (MOVETO(TBOARD R,PIECEON(TBOARD R,FROM MOVE P),FROM MOVE P,TO MOVE P)∧
     ((SIMPLE MOVE P⊃POS(R,TO MOVE P)=EMPTY)∧
     ((CAPTURE MOVE P⊃(WHITEPIECE TAKEN MOVE P≡WHITETURN P))∧
     ¬(CAPTURE MOVE P≡SIMPLE MOVE P))))));;
DEFINE PREVLEGAL:
  ∀P SQ X.(((WHITEPIECE X≡WHITETURN P)∧POS(P SQ)=X∧¬POS(P0 SQ)=X)⊃∃Q.PREVPOS P=Q);;
DEFINE STAYS:
  ∀R P SQ X.((SUCCESSOR(R P)∧(WHITEPIECE X≡WHITETURN P)∧POS(P SQ)=X)⊃POS(R SQ)=X);;
DEFINE NAMED_WPAWNS:∀P.(BOARD(P,QBUD)⊃(POS(P,'(7 . 1))=WQRP∧(POS(P,
'(6 . 2))=WQNP∧(POS(P,'(7 . 3))=WQBP∧((POS(P,'(2 . 3))=WKP∨POS(P,'(2 
. 3))=WQP)∧(((POS(P,'(6 . 4))=WKP∨POS(P,'(6 . 4))=WQP)∧¬(POS(P,'(2 . 
3))=POS(P,'(6 . 4))))∧(POS(P,'(7 . 6))=WKBP∧(POS(P,'(6 . 7))=WKNP∧POS
(P,'(7 . 8))=WKRP))))))))  ;;
MARK M1;